Nuprl Lemma : assert-d-eq-Loc
11,40
postcript
pdf
i
,
j
:Id. (
i
=
j
)
(
i
=
j
)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
i
=
j
,
P
Q
,
,
P
Q
,
t
T
,
x
.
t
(
x
)
,
P
&
Q
,
x
(
s
)
Lemmas
all
functionality
wrt
iff
,
Id
wf
,
iff
wf
,
assert
wf
,
eqof
wf
,
id-deq
wf
,
iff
functionality
wrt
iff
,
deq
property
origin
i, j:Id. (i = j) 
(
i = j) i, j:Id. (i = j) (i = j) x:A. B(x) Q Q
Q
T
x. t(x)